CS 206           HANDOUT # 34             JUNE 3, 1974

IMPORTANT: See last page for OPTIONAL homework assignment.
This homework assignment need not be turned in; however,
you can expect a simple question on micro-PLANNER on the
final exam.

		Beginner's Guide to Micro-PLANNER

consisting of various plagiarisms from PLNR.RPO[UP,DOC] (Richard Orban),
SAILON 67 (Bruce Baumgart), and MIT class notes for 6.258 (Pat Winston),
along with an extra example or two.

 	Micro-PLANNER is an implementation of a subset of Carl 
Hewitt's language, PLANNER, by Gerald Sussman, Terry Winograd, and 
Eugene Charniak in LISP.  It is a goal-directed language, and also
has several other features which augment LISP, including backup and
an associative data base.

	Micro-PLANNER is oriented toward the accomplishment of 
tasks (or goals) which may in fact be broken down into subtasks
(subgoals).  When a goal in a PLANNER program is activated, it may
be satisfied by any number of objects in the data base or by any
number of theorems (the counterpart of procedures).  A backup 
mechanism is provided so that one of the possibilities is tried,
and then, if as a consequence a failure occurs, another is tried,
etc.  Furthermore, the data and theorems need not be referenced
explicitly but rather by specifying "the datum (or procedure) which

	Note that the convention for calling "theorems" pushes the
user in the direction of thinking about what he wants done rather
than how to do it; this should and does lead to clearer programs.
The provision of backtracking and pattern-matching in Micro-PLANNER, 
highly useful for a.i.-type programs but often a hassle to work into 
a LISP program, is an additional bonus to the user.
	Micro-PLANNER consists of an associative memory of assertions
and theorem patterns, combined with a pushdown memory of variable
bindings, along with the LISP memory structures of property lists and
values.  We will first examine the Micro-PLANNER functions for using
and manipulating its associative data base.

	Facts are entered into the data base using THASSERT.  One 
writes (THASSERT (A ON B)) to place the fact (A ON B) into the data
base.  The fact need not be a list of three atoms; any S-expression
will do.  

	To remove a fact from the data base, one uses the function
THERASE.  For example, saying (THERASE (A ON B)) causes the fact
(A ON B) to be deleted from the data base.

	To get a fact out of the data base, one can write something
like (THGOAL (A ON ?)) to answer the question "Is A on anything?"
By definition, the expression (THGOAL (A ON ?)) is said to succeed or
fail depending on whether or not there is a matching fact in the data
base.

	Consider again the question "Is A on anything?" or in logic,
(EXISTS (Y) (A ON Y)).  It can also be expressed in Micro-PLANNER as
(THPROG (Y) (THGOAL (A ON (THV Y)))).  Notice that THPROG (Micro-
PLANNER's equivalent of a LISP PROG, complete with GO statements, 
labels, RETURN, etc.) acts as an existential quantifier.  It provides
a binding-place for the variable Y, but does not initialize it -- it
leaves it in a state particularly marked as unassigned.  To answer the
question, we ask Micro-PLANNER to evaluate the entire THPROG expression
above.  To do this it starts by evaluating the THGOAL expression.  The
data base is searched for an assertion of the form (A ON (THV Y)); the
assertion (A ON B) is found, the variable Y is assigned the constant B,
(A ON B) is returned, and the THPROG succeeds.

	The strange function, THV, is the way of specifying that Y is 
a variable and not a constant as A, B, and ON are, and is part of
Micro-PLANNER's pattern matching capabilities.  If we ask Micro-
PLANNER to prove a goal of the form (A X), there is no obvious way of
knowing whether A and X are constants or variables.  LISP solves this
problem by using the function QUOTE to indicate constants.  In pattern
matching this is inconvenient and makes most patterns much bulkier and
more difficult to read.  Instead, Micro-PLANNER uses the opposite
convention -- a constant is represented by the atom itself, while a
variable must be indicated by adding an appropriate function.  This
function differs according to the exact use of the variable in the
pattern, but for the time being let us just accept THV as a function
indicating a variable.

	We see in Micro-PLANNER a feature which assigns pattern
variables at the same time a match is found.  For instance, B was 
assigned to the variable Y in the above example.  If a variable like
Y already has an assignment going into a THGOAL, then the search is 
for a fact with Y's assignment substituted in for instances of (THV Y).
Suppose the data base has facts reflecting the situation diagrammed
below.  Then in the first THGOAL, (THV Y) is matched as if it were an
ordinary ? since at that point it has no assignment.  But in the 
second THGOAL, (THV Y) has the assignment of B which was attached in
the successful match of the first THGOAL.  Therefore in the second
THGOAL, (THV Y) acts as if it were B and the data base is searched 
for a fact of the form (B ON ?).  Since B is indeed on something else,
both the first and the second THGOALs succeed.

	_____
	|   |
	| A |			(THPROG (Y)
	|___|
	|   |				(THGOAL (A ON (THV Y)))
	| B |
	|___|____			(THGOAL ((THV Y) ON ?)) )
	|       |
	|   C   |
	|_______|


	Now suppose the situation is altered a bit so that A is on D
as well as B.  Then there is no way to know how the first THGOAL 
would assign (THV Y).  It may come out of the match assigned either
to D or to B.  If (THV Y) comes out of the match assigned to B then
the second THGOAL succeeds as before.  If, however, the first match
assigns (THV Y) to D, then the second THGOAL fails and we have our
first instance of a failure initiated backup.  Under these conditions,
Micro-PLANNER automatically retraces the computation to the last place
where a decision was made.  In this case, the selection of D rather
than B in the first THGOAL was the last decision and the automatic
backup need go only one step.  If any choices are yet untried at the
decision point, then a new choice is made and control proceeds in the
normal forward direction again.  Consequently the locus of activity in
the event that D is the first assignment of Y is as shown by the 
dotted line:

				    |
				(THPROG (Y)
				    \____     __
					 \   /  \
	_________________		(THGOAL (A ON (THV Y)))
	|		|		  ↓  ↑  ↓
	|       A	|     		(THGOAL ((THV Y) ON ?)) )
	|_______________|		  \__/  |
	|    |      |   |			|
	|    |      | B |			|
	| D  |    __|___|_______		|
	|    |   |		|		↓
	|    |   |	C	|
	|____|	 |______________|


If neither B nor D turned out to be on any other thing, then both
choices at the first THGOAL would lead to failure and backup would 
propagate directly up to whatever code precedes the THPROG in search
of a still earlier decision point where there might be some alternative
yet to be explored.

	It is important to realize that everything done is undone when
backup moves up through a series of actions.  Backing over a THASSERT
pulls the assertion out of the data base and backing over a THERASE
similarly puts the erased assertion back in the data as if it were 
never removed.
	Theorems in Micro-PLANNER are the equivalent of subroutines,
which can be called by pattern as well as by name.  There are three
kinds:  consequent theorems, for establishing goals; antecedent 
theorems, for expanding on assertions; and erasing theorems, for
expanding on erasures.  Theorems are defined by (DEFPROP <name>
<body> THEOREM); they are added to the data base using THASSERT and
removed using THERASE.

	For an example, we can use Adam and Eve, both of whom are 
known to be human by way of the assertions (HUMAN ADAM) and (HUMAN
EVE).  Now to show that Adam is fallible, we would check to see if 
the fact is already known, i.e., already noted in the data base, by
(THGOAL (FALLIBLE ADAM)).  This will fail.

	However, with hardly any additional hassle, Micro-PLANNER can
be made to not give up so easily.  It will search for some program
that can help establish that Adam is fallible.  The program below
expresses the idea that showing something to be fallible can be done
by showing that it is human:

	(DEFPROP GS 				I.e. only if X is
	    (THCONSE (X) (FALLIBLE (THV X))	fallible can X be
		(THGOAL (HUMAN (THV X))) )	human, or if X is 
	 THEOREM)				human then X is 
	(THASSERT GS)				also fallible.

Features of this example:
1.  The name of the subroutine immediately follows DEFPROP; the name of 
    this theorem is GS (mnemonic for Goal Subroutine).
2.  THCONSE defines the theorem to be a consequent theorem; that is, if 
    the conditions of the theorem are satisfied, then the given goal is
    established.  
3.  Following the type of the theorem is a list of variables to be bound
    on entry to the subroutine.  Variables are either unbound, unassigned,
    or assigned; the binding of a variable does not assign it a value,
    but specifies that any value picked up during the action of the 
    subroutine will be lost on exit.
4.  Following the list of variables to be bound is the pattern which in
    some sense describes what goals the subroutine is relevant to.  In
    particular, the subroutine is relevant to establishing a goal found
    stated within a THGOAL only if the subroutine's pattern successfully
    matches the THGOAL pattern.  In this case, the subroutine pattern
    (FALLIBLE (THV X)) matches the goal pattern in (THGOAL (FALLIBLE 
    ADAM)).  Additionally, the successful match assigns variables if
    possible.  In this case, the subroutine GS could be involved by an
    attempt to satisfy the goal (THGOAL (FALLIBLE ADAM)) and would 
    result in an assignment of X to ADAM.
5.  Following the pattern is a list of exactly those things that must
    succeed to make the subroutine succeed.  The THGOAL succeeds if it
    invokes a theorem which succeeds.
6.  THASSERT adds the theorem to the associative data base of theorems.
The following THGOAL statement would use the above theorem:
	(THGOAL (FALLIBLE ADAM) (THTBF THTRUE))
where (THTBF THTRUE) is advice that causes the evaluator to try all
theorems whose consequent is of a form which matches the goal.  The
above THGOAL statement, when evaluated, causes a data base search to be
made, which in this case fails.  Then GS is noted to be relevant by way
of a natch of its pattern against the goal pattern.  X is simultaneously
assigned to ADAM.  GS tries to find (HUMAN ADAM) in the data and 
succeeds.  This means that the theorem succeeds and this in turn means
that the goal succeeds.

	This leaves us prepared for a slightly more complex case in 
which we are not simply trying to show something about Adam, but 
instead to find someone satisfying some criteria.  In particular, let
us add a fact to the data base so that the known facts are
	(HUMAN EVE)
	(HUMAN ADAM)
	(SINNER EVE)
Given a data base with these facts, suppose we look for a fallible 
sinner.  The fallible sinner can be sought by a pair of goals in a 
THPROG:
	(THPROG (Y)
	    (THGOAL (FALLIBLE (THV Y)) (THTBF THTRUE))
	    (THGOAL (SINNER (THV Y)) (THTBF THTRUE)) )

Since there are no things known by direct data base search to be 
fallible, the first THGOAL in the THPROG causes a call to GS whose
pattern matches the goal pattern.  On entering GS, there is as yet
nothing to assign the pattern variable X to since it matches the as yet
unassigned Y.  The match does however marry the variables together in a
sense because now any assignment given to X will also be given to Y at
the same time.  GS now tries to find something that matches (HUMAN (THV
X)) in order to supply the calling goal with something fallible. 
Suppose it first happens on ADAM.  Then the data base match with (HUMAN
ADAM) assigns both X and Y to ADAM.

	Since GS succeeds with ADAM, the goal (THGOAL (FALLIBLE (THV Y))
(THTBF THTRUE)) succeeds and control moves to (THGOAL (SINNER (THV Y))
(THTBF THTRUE)).  But this goal cannot be satisfied as there is nothing
of the form (SINNER ADAM) in the data base and there is no relevant
subroutine.  Backup begins, and moves into the subroutine GS where 
control came from; it is important to realize that backup proceeds to
where the action was rather than straight up the page.  In GS, a 
decision is found pulling ADAM instead of EVE out of the data base.  
This decision is reconsidered and a new choice is made, causing both
X and Y to be reassigned to EVE.  Now the new assignment of Y permits
the second THGOAL in the THPROG to succeed, which results in success for
the THPROG.

	This ADAM and EVE example suggests that Micro-PLANNER eases 
the casting of knowledge into procedural form.  In fact, the Micro-
PLANNER language not only simplifies the task of programming 
knowledge -- it also allows that programming to include information
about how the knowledge is to be used.  So far we have considered
only one way the fact "all humans are fallible" might be used (namely
to show something is fallible).  But another thing to do, particularly
if we know it is often necessary to know if something is fallible, is
to make a note that something is fallible automatically when that
something is for some reason shown to be human.  For this kind of use,
THANTE is used instead of THCONSE.  Thus the following subroutine
could be activated (depending on things like THTBF) whenever something
is shown to be HUMAN, and would assert additionally that the thing is
fallible:
	(DEFPROP AS 
	    (THANTE (X) (HUMAN (THV X))		I.e. if X is human,
		(THASSERT (FALLIBLE (THV X))))	then X is also
	 THEOREM)				fallible.

	An important problem is that of maintaining a data base with
a reasonable amount of material.  For instance, consider two ways of 
using the statement that all humans are fallible.  The first way is to
simply use it whenever we are faced with the need to prove (FALLIBLE
(THV X)).  Another way might be to watch for a statement of the form
(HUMAN (THV X)) to be asserted, and to immediately assert (FALLIBLE
(THV X)) as well.  There is no abstract logical difference, but the
impact on the data base is tremendous.  The more conclusions we draw
when information is asserted, the easier proofs will be, since they
will not have to take the steps to deduce these consequences over and
over again.  However, since we don't have infinite speed and size, it
is clearly folly to think of deducing and asserting everything possible
(or even everything interesting) about the data when it is entered. 
Part of the knowledge which Micro-PLANNER should have of a subject,
then, is what facts are important, and when to draw consequences of an
assertion, using THANTE theorems like the theorem AS above.
	Examples from Winograd's block world:

(THGOAL (#IS ? #BLOCK))			Find a block.

(THGOAL (#IS ? #PYRAMID))		Find a pyramid.

(THPROG (X)				Find a red block.
    (THGOAL (#IS (THV X) #BLOCK))	If there are more red things
    (THGOAL (#COLOR (THV X) #RED)))	 than blocks, the two THGOALs
					 should be reversed.

(THPROG (X)				Put a red block at position Y.
    (THGOAL (#IS (THV X) #BLOCK))
    (THGOAL (#COLOR (THV X) #RED))
    (THGOAL (#PUT (THV X) (THV Y))) )

(THPROG (B1 B2 P1)			Find a pyramid sitting on
    (THGOAL (#IS (THV P1) #PYRAMID))	 at least two blocks.
    (THGOAL (#SUPPORT (THV B1) (THV P1))
    (THGOAL (#SUPPORT (THV B2) (THV B1))
    (THGOAL (#IS (THV B1) #BLOCK))
    (THGOAL (#IS (THV B2) #BLOCK))

It should be noted that this program is not very efficient in case there
are pyramids sitting lots of things beside blocks.  In some sense there
is a tendency in using Micro-PLANNER to be seduced into inefficiency of 
this exhaustive depth-first tree search flavor.  In some cases, THGOAL
reordering within the THPROG helps; for example, if there were very few
blocks, moving the fourth and fifth THGOALs in front of the #SUPPORT
THGOALS would improve the searching.

(THPROG (RB GB)				Find a green block sitting on
    (THGOAL (#IS (THV GB) #BLOCK))	 a red block, and remove it.
    (THGOAL (#SUPPORT (THV RB) (THV GB)))
    (THGOAL (#IS (THV RB) #BLOCK))
    (THGOAL (#CLEARTOP (THV RB))) )

(DEFPROP ARCHTHM			Define an arch (two blocks
    (THCONSE (S1 S2 TOP)		 supporting another block).
     (ARCH (THV S1) (THV S2) (THV TOP))
	(THGOAL (#SUPPORT (THV S1) (THV TOP)))
	(THGOAL (#SUPPORT (THV S2) (THV TOP)))
	(THGOAL (#IS (THV S1) #BLOCK))
	(THGOAL (#IS (THV S2) #BLOCK))
	(THGOAL (#IS (THV TOP) #BLOCK))
     )
THEOREM)

Note that, if a check of relevant theorems were desired to prove one of
the above THGOALs, the advice (THTBF THTRUE) should be added to the end.
(For more information on "advice", see the other two manuals; it's 
called "recommendations" there).
Other useful Micro-PLANNER functions:

(THNOT <e>)
	THNOT succeeds if and only if its argument fails.

(THAND <e1> ... <en>) 
	THAND  fails  unless  each  of its subexpressions succeeds in
sequence, allowing for backup.  It is just like  THPROG  except  that
there are no variable declarations or tags allowed.
  
(THOR <e1> ... <en>) 
	THOR succeeds if at least one of its subexpressions succeeds.
Basically, it CDRs down the list looking for a winner and if it finds
one it succeeds, returning its value as  the  PLANNER  value.   If  a
failure  propagates back to it, however, it continues CDRing from the
point it left off until it finds another winner or it loses.
   
(THCOND <pair1> ... <pair n>) 
	THCOND  is  the  PLANNER  analogue  of  COND  in LISP.  As in
Stanford LISP the "pairs" needn't be.  Basically THCOND executes  the
CAR of each pair until one succeeds.  The THCOND will then succeed if
all the rest of that "pair" succeeds (like a THAND) else THCOND  will
fail.
  
(THSETQ <var1> <e1> ... <varn> <en>)
	Variable 1 is set to the value of e1, ..., and variable n is
set to the value of en.  All of it is undone if failure backs up to it.

(THSUCCEED THEOREM) or (THFAIL THEOREM)
	These commands propagate success or failure out of a theorem.

(THGO <label>)
	As in LISP, except it's undone when failure backs up to it.

(THV  <variable name>)  (THNV <variable name>) 
	These LISP functions get the PLANNER value of the variable
whose name is given.  They differ in effect, if used in a pattern match,
whenever the specified variable already has been assigned a PLANNER
value.  In this case, when THV is used, the value of the variable must
match for the pattern match to succeed; when THNV is used, the value of
the variable need not match, and the variable is reassigned a value 
that would.  THNV is useful in a loop, to initialize a variable (see
below).
Examples:

(THPROG (X)				Find either a red or a white
    (THGOAL (#IS (THV X) #BLOCK))	 block on the table.
    (THOR (THGOAL (#COLOR (THV X) #RED))
	  (THGOAL (#COLOR (THV X) #WHITE)))
    (THGOAL (#SUPPORT !TABLE (THV X))) )

(THPROG (X)				Find a block without anything
    (THGOAL (#IS (THV X) #BLOCK))	 red on it.
    (THNOT
	(THPROG (Y)
	    (THGOAL (#COLOR (THV Y) #RED))
	    (THGOAL (#SUPPORT (THV X) (THV Y))) )) )

	To date the most frequent use of backup by Micro-PLANNER
programmers has been in filtering some particular object or other
entity out of the data base as in the following code fragment:
	(THGOAL (#IS (THV B1) #BLOCK))
	(THNOT (THAND
		(THGOAL (#IS (THV B2) #BLOCK))
		(BIGGERP B2 B1) ))
To move beyond the first line of code, it is clear that B1 must be a
block.  Similarly, to traverse the first element of the THAND, B2
must be a block.  Now the predicate BIGGERP (a LISP predicate supplied
by the user) may succeed or fail.  If it succeeds, then B2 is bigger
than B1, so the THNOT fails; this in turn causes a new choice for B1.
On the other hand, if BIGGERP fails, then the failure causes direct
backup in search of another B2.  If there is another assignment for
B2, the program moves forward again to try the BIGGERP another time.
Thus if any B2 is available that makes the BIGGERP succeed, the result
is converted to a failure by the flipping THNOT!  But if no B2 can be
found, then the THNOT converts this to a success.  Therefore no 
complete movement through the code is possible until B1 is assigned to
the biggest block.
Sample dialogue:

0!*(THASSERT (ROSES ARE RED))		You input after !*.
((ROSES ARE RED))			Assertion returns in a list.

0!*(THSETQ (THV X) @RED)		Assign X a PLANNER value.
RED

0!*(THSETQ (THNV Y) @BLACK)		THNV and THV the same since
BLACK					  Y still unassigned.

0!*(THSETQ (THV Z) @UNASSIGNED)		Merely declares Z; unassigned
UNASSIGNED				  variable has val UNASSIGNED.

0!*(THGOAL (ROSES ARE (THV X)))		THV causes value of X to be
((ROSES ARE RED))			  relevant in pattern match.

0!*(THGOAL (ROSES ARE (THV Y)))		Data base searched for (ROSES
NIL					  ARE BLACK) since THV used.

0!*(THV Y)
BLACK

0!*(THGOAL (ROSES ARE (THNV Y)))	Value of Y not checked at all;
((ROSES ARE RED))			  Y is reassigned if necessary
					  to make the pattern match.
0!*(THV Y)
RED					Sure enough, Y was reassigned.

0!*(THGOAL (ROSES ARE (THV Z)))		Since Z was unassigned, it is
((ROSES ARE RED))			  also given a value by the
					  pattern match, even though
0!*(THV Z)				  THV was used.
RED
A sample theorem and its trace:

(DEFPROP CLEARTOP			Clears the top of block X.
    (THCONSE (X Y) (#CLEARTOP (THV X))
L	(THCOND
		For any block Y sitting on X, clear everything off Y, then
		 get rid of Y.  Note that there may be more than one thing
		 sitting on X, which is the reason for the loop.
	    ((THGOAL (#SUPPORT (THV X) (THNV Y)))
	     (THGOAL (#CLEARTOP (THV Y)) (THTBF THTRUE))
	     (THGOAL (#GET-RID-OF (THV Y)) (THTBF THTRUE))
	     (THGO L))
		If nothing on X, then done, so assert X clear.  The
		  assertion need not be done if the information that
		  X is clear won't ever be needed again.
	    ( T (THASSERT (#CLEARTOP (THV X))))) )
 THEOREM)
 0*(THGOAL (#CLEARTOP !B1) (THTBF THTRUE))

TRYING GOAL G1 (#CLEARTOP !B1)
 TRYING GOAL G2 (#SUPPORT !B1 (THNV Y))
 G2 SUCCEEDED ((#SUPPORT !B1 !B2))
 TRYING GOAL G3 (#CLEARTOP !B2)
 G3 SUCCEEDED ((#CLEARTOP !B2))
 TRYING GOAL G4 (#GET-RID-OF !B2)
  TRYING GOAL G5 (#FINDSPACE !TABLE (100 100 100) !B2 (THNV Y))
  G5 SUCCEEDED (#FINDSPACE !TABLE (100 100 100) !B2 (64.0 544.0 0.0))
  TRYING GOAL G6 (#PUT !B2 (64.0 544.0 0.0))
   TRYING GOAL G7 (#AT !B2 (64.0 544.0 0.0))
   G7 FAILED 
   TRYING GOAL G10 (#GRASP !B2)
    TRYING GOAL G11 (#GRASPING !B2)
    G11 FAILED 
    TRYING GOAL G12 (#CLEARTOP !B2)
    G12 SUCCEEDED ((#CLEARTOP !B2))
    TRYING GOAL G13 (#GRASPING (THNV Y))
    G13 FAILED 
    TRYING GOAL G14 (#MOVEHAND2 (96.0 96.0 200))
    G14 SUCCEEDED (#MOVEHAND2 (96.0 96.0 200))
   G10 SUCCEEDED (#GRASP !B2)
   TRYING GOAL G15 (#MOVEHAND (96.0 576.0 64.0))
    TRYING GOAL G16 (#GRASPING (THV X))
    G16 SUCCEEDED ((#GRASPING !B2))
    TRYING GOAL G17 (#AT !B2 (THNV W))
    G17 SUCCEEDED ((#AT !B2 (100 100 100)))
    TRYING GOAL G20 (#SUPPORT !B2 (THNV Y))
    G20 FAILED 
    TRYING GOAL G21 (#SUPPORT (THV Y) !B2)
    G21 SUCCEEDED ((#SUPPORT !B1 !B2))
    TRYING GOAL G22 (#SUPPORT !B1 (THV Z))
    G22 FAILED 
    TRYING GOAL G23 (#SUPPORT !B1 !B2)
    G23 FAILED 
    TRYING GOAL G24 (#MANIP !TABLE)
    G24 FAILED 
    TRYING GOAL G25 (#MOVEHAND2 (96.0 576.0 64.0))
    G25 SUCCEEDED (#MOVEHAND2 (96.0 576.0 64.0))
   G15 SUCCEEDED (#MOVEHAND (96.0 576.0 64.0))
   TRYING GOAL G26 (#UNGRASP)
    TRYING GOAL G27 (#GRASPING (THV X))
    G27 SUCCEEDED ((#GRASPING !B2))
    TRYING GOAL G30 (#SUPPORT ? !B2)
    G30 SUCCEEDED ((#SUPPORT !TABLE !B2))
   G26 SUCCEEDED (#UNGRASP)
  G6 SUCCEEDED (#PUT !B2 (64.0 544.0 0.0))
 G4 SUCCEEDED (#GET-RID-OF !B2)
 TRYING GOAL G31 (#SUPPORT !B1 (THNV Y))
 G31 FAILED 
G1 SUCCEEDED (#CLEARTOP !B1)
(#CLEARTOP !B1) 
              OPTIONAL HOMEWORK ASSIGNMENT

As in the CLEARTOP example, assume you have a data base which
consists of assertions like (#SUPPORT x y) and possibly (#CLEARTOP y).
you may assume the #SUPPORT assertions are consistant. 

 Write a micro-PLANNER theorem (of the THCONSE type) which will
empty THE box (there is only one box); the general algorithm 
should be: for everything in the box, clear off its top and
  THEOREM)


This should be even simpler than CLEARTOP. Note
that X is in the box if (THGOAL (#SUPPORT BOX X)) succeeds.